\begin{tabbing}
sendMinimalR\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $l$; ${\it ds}_{1}$; ${\it ds}_{2}$; $P$; $Q$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=weakPrecondSendR\{\$a,\$tg\}($T$;$\mathbb{N}$;$l$;${\it ds}_{1}$;$\lambda$$s$,$m$. $\neg$$P$($s$,$m$) \& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $P$($s$,$n$));$f$)\+
\\[0ex].\=weakPrecondSendR\{\$a,\$tg\}($\mathbb{N}$;$\mathbb{N}$;lnk{-}inv($l$);${\it ds}_{2}$;$\lambda$$s$,$m$. $\neg$$Q$($s$,$m$)\+
\\[0ex]\& ($\forall$$n$:$\mathbb{N}$. $n$$<$$m$ $\Rightarrow$ $Q$($s$,$n$));$\lambda$$s$,$m$. $m$)
\\[0ex].nil)
\-\-
\end{tabbing}